1. Technical Field
The present invention relates to concurrent program verification and, in particular, to systems and methods for symbolically checking assertions in concurrent programs in a compositional manner.
2. Description of the Related Art
A variety of methods have been developed for checking properties of concurrent programs. Analyzing all thread interleavings is a bottleneck: all interleavings of global object accesses that may affect a property are be checked. Most methods for verifying concurrent software symbolically encode the transition relation of the program in terms of a first-order or propositional logic formula and use a satisfiability/satisfiability-modulo-theory (SAT/SMT) solver to find thread interleavings that violate the property.
Other approaches either (i) abstract the transition relations of individual threads and iteratively refine the abstractions based on counterexamples found, (ii) abstract and refine the set of reachable states of each thread, (iii) use assume-guarantee reasoning based on computing environment assumptions for each thread, or (iv) unroll the transition relation of the concurrent program in a context-bounded manner. Methods of type (i) are incomplete with respect to proving general assertions since they are not able to expose all of the relations between local states of threads. Methods of type (ii) have not been applied to real-life C programs and may suffer from large number of refinement iterations. Methods of type (iii) are extremely expensive due to the cost to computing environment assumptions automatically. Methods of type (iv) are context-bounded.
The task of searching through large number of interleavings, together with the complex data-flow in individual threads, over-burdens the constraint solver and thus impedes the scalability of the prior approaches.